Notes (Week 7 Tuesday)

1. Trace properties
- 1.1. Safety property: I will never run out of money.
- 1.2. Liveness property: I will eventually have over $1000.
2. Exception handling - General form
3. Exception handling - Example from slides

These are notes I made during the lecture, with some cleanups made after.

1. Trace properties

Supposing all traces are infinite (by repeating the final state forever for finite ones), a property is a set of traces - intuitively, they are the traces that satisfy the property.

1.1. Safety property: I will never run out of money.

This trace satisfies the property:

$100 ↦ $150 ↦ $90 ↦ ... (* infinite trace for which money > $0
                           at all states: good *)

This trace prefix violates the property:

$100 ↦ $150 ↦ $90 ↦ $0 (bad)

All traces that extend this prefix also violate the property (i.e. they are not in set of traces that characterise the property).

In general, safety properties can be violated by a finite prefix of a trace.

1.2. Liveness property: I will eventually have over $1000.

This trace prefix satisfies the property:

$100 ↦ $150 ↦ $90 ↦ $1001 (good)

All traces that extend this prefix also satisfy the property (i.e. they are in the set of traces that characterise the property).

This trace violates the property:

$100 ↦ $150 ↦ $90 ↦ ... (* infinite trace for which money ≤ $1000
                           at all states: bad *)

In general, you need a full (infinite) trace to show a liveness property is violated - a finite prefix isn't enough.

2. Exception handling - General form

try
  (* do something that might raise exception *)
handle x ⇒ 
  (* handle the exception identifier x *)

3. Exception handling - Example from slides

3.1. Concrete syntax

try
  if y ≤ 0 then
    raise DivisorError
  else
    (x/y)
handle err ⇒ −1

3.2. Abstract syntax

Try (If (y ≤ 0) (Raise DivisorError) (Quot x y)) (err. -1) : int

3.3. Example of dynamic semantics of exception handling

Remember, ∘ is the symbol for the empty stack.

I'm going to leave x and y as variables here, but presumably if this Try block was inside a function, then instead of x and y we'd have (Num x) and (Num y) here for some actual numerical values x and y, and instead of the empty stack ∘ we'd have a bunch of information about the Try block's calling context.

Note, this example applies the original, less efficient dynamic semantics transition rules for exception handling in the C machine (given on the slide titled "Dynamic Semantics") - not the more efficient version that adds a second stack for exceptions (given on the slide titled "Efficient Exceptions").

∘ ≻ (Try (If (y ≤ 0) (Raise DivisorError) (Quot x y)) (err. (Num -1)))

↦c

(Try □ (err. (Num -1))) ▹ ∘
  ≻ (If (y ≤ 0) (Raise DivisorError) (Quot x y))

↦c

(If □ (Raise DivisorError) (Quot x y)) ▹ (Try □ (err. (Num -1))) ▹ ∘
  ≻ (y ≤ 0)

3.3.1. Case 1: y ≤ 0

(If □ (Raise DivisorError) (Quot x y)) ▹ (Try □ (err. (Num -1))) ▹ ∘
  ≻ (y ≤ 0)

↦c ... ↦c

(If □ (Raise DivisorError) (Quot x y)) ▹ (Try □ (err. (Num -1))) ▹ ∘
  ≺ True

↦c

(Try □ (err. (Num -1))) ▹ ∘ ≻ Raise DivisorError

↦c

(Raise □) ▹ (Try □ (err. (Num -1))) ▹ ∘ ≻ DivisorError

↦c

(Try □ (err. (Num -1))) ▹ ∘ ≺≺ DivisorError

↦c

∘ ≻ (Num -1)

↦c

∘ ≺ (Num -1) : int

3.3.2. Case 2: y > 0, and say x/y = z where z is a numerical value

(If □ (Raise DivisorError) (Quot x y)) ▹ (Try □ (err. (Num -1))) ▹ ∘
  ≻ (y ≤ 0)

↦c ... ↦c

(If □ (Raise DivisorError) (Quot x y)) ▹ (Try □ (err. (Num -1))) ▹ ∘
  ≺ False

↦c

(Try □ (err. (Num -1))) ▹ ∘ ≻ (Quot x y)

↦c ... ↦c

(Try □ (err. (Num -1))) ▹ ∘ ≺ (Num z)

↦c

∘ ≺ (Num z) : int